M1  M2
== (M1.1  M2.1 & (M1.2).1  (M2.2).1)
== c ((M1.2.2).1  (M2.2.2).1
== c & (M1.2.2.2).1  (M2.2.2.2).1
== c & (M1.2.2.2.2).1  (M2.2.2.2.2).1
== c & (M1.2.2.2.2.2).1  (M2.2.2.2.2.2).1
== c & (M1.2.2.2.2.2.2).1  (M2.2.2.2.2.2.2).1
== c & (M1.2.2.2.2.2.2.2).1  (M2.2.2.2.2.2.2.2).1
== c & (M1.2.2.2.2.2.2.2.2).1  (M2.2.2.2.2.2.2.2.2).1
== c & (M1.2.2.2.2.2.2.2.2.2).1  (M2.2.2.2.2.2.2.2.2.2).1
== c & (M1.2.2.2.2.2.2.2.2.2.2).1  (M2.2.2.2.2.2.2.2.2.2.2).1
== c & (M1.2.2.2.2.2.2.2.2.2.2.2).1  (M2.2.2.2.2.2.2.2.2.2.2.2).1) 

latex

---

clarification:

ma-sub{i:l}
ma-sub(M1; M2)
== (fpf-sub(Id; x.Type{i}; IdDeq; (M1.1); (M2.1))
== & fpf-sub(Knd; x.Type{i}; KindDeq; ((M1.2).1); ((M2.2).1)))
== c (fpf-sub(Id; x.(fpf-cap(M2.1;IdDeq;x;Void)); IdDeq; ((M1.2.2).1); ((M2.2.2).1))
== c & fpf-sub(Id; a.(State(M2.1)); IdDeq; ((M1.2.2.2).1); ((M2.2.2.2).1))
== c & fpf-sub((:Knd  Id);
== c & fpf-sub(kx.(State(M2.1)Valtype((M2.2).1;kx.1)fpf-cap(M2.1;IdDeq;kx.2;Void));
== c & fpf-sub(product-deq(Knd;Id;KindDeq;IdDeq);
== c & fpf-sub(((M1.2.2.2.2).1);
== c & fpf-sub(((M2.2.2.2.2).1))
== c & fpf-sub((:Knd  IdLnk);
== c & fpf-sub(kl.((tg:Id
== c & fpf-sub( (State(M2.1)Valtype((M2.2).1;kl.1)
== c & fpf-sub( (fpf-cap((M2.2).1;KindDeq;rcv(kl.2,tg);Void) List))) List);
== c & fpf-sub(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);
== c & fpf-sub(((M1.2.2.2.2.2).1);
== c & fpf-sub(((M2.2.2.2.2.2).1))
== c & fpf-sub(Id; x.(Knd List); IdDeq; ((M1.2.2.2.2.2.2).1); ((M2.2.2.2.2.2.2).1))
== c & fpf-sub((:IdLnk  Id);
== c & fpf-sub(ltg.(Knd List);
== c & fpf-sub(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);
== c & fpf-sub(((M1.2.2.2.2.2.2.2).1);
== c & fpf-sub(((M2.2.2.2.2.2.2.2).1))
== c & fpf-sub(Knd; k.(Id List); KindDeq; ((M1.2.2.2.2.2.2.2.2).1); ((M2.2.2.2.2.2.2.2.2).1))
== c & fpf-sub(Knd; k.(IdLnk List); KindDeq; ((M1.2.2.2.2.2.2.2.2.2).1); ((M2.2.2.2.2.2.2.2.2.2).1)
== c & fpf-sub()
== c & fpf-sub(Id; x.(Knd List); IdDeq; ((M1.2.2.2.2.2.2.2.2.2.2).1); ((M2.2.2.2.2.2.2.2.2.2.2).1))
== c & fpf-sub(Id;
== c & fpf-sub(x.FinProbSpace;
== c & fpf-sub(IdDeq;
== c & fpf-sub(((M1.2.2.2.2.2.2.2.2.2.2.2).1);
== c & fpf-sub(((M2.2.2.2.2.2.2.2.2.2.2.2).1))) 

latex

Definitions	A c B, Type, , , State(ds), x:AB(x), Valtype(da;k), f(x)?z, rcv(l,tg), Void, x:A  B(x), product-deq(A;B;a;b), IdLnkDeq, IdLnk, KindDeq, P & Q, type List, Knd, f  g, Id, FinProbSpace, IdDeq, t.1, t.2
FDL editor aliases	ma-sub